近日，初创公司Axiom震撼了整个硅谷AI圈，也让科技界为之瞩目。在来自中国广东的25岁女孩洪乐潼的带领下，这家成立不足两年、团队仅20余人的公司，在用数学解决AI幻觉的冷门赛道闯出了一条路，拿下2亿美元A轮融资，一跃成为估值16亿美元的独角兽。

这不仅是一个鼓舞人心的创业神话，更触及了当下AI行业最痛的神经——当所有人都在AI大模型应用赛道上狂飙猛进时，那个潜伏在暗处、极易引发灾难性后果的“AI幻觉”却常被选择性忽略。面对这一随时可能动摇AI信任根基的隐患，中欧国际工商学院决策科学与管理信息系统教授谭寅亮，深度剖析了AI幻觉的生成机制和切实可行的破局之道。

当整个AI行业都在狂热追求更大的参数模型、更逼真的生成能力时，洪乐潼和她的初创公司Axiom，却转身去做了一件AI圈里最冷门，也最难啃的事——解决AI幻觉。

Axiom所采用的方法叫“形式化验证”。说白了，就是要把AI模糊的、概率性的推导过程，变成每一步都可以用数学和逻辑进行检查、证明和追责的确定性过程。

但要真正理解Axiom为什么如此受追捧，需要先建立一种认知：AI幻觉不是一个单纯的“缺点”，而是一个“特点”。

01

正确理解AI幻觉

很多人在发现大语言模型“一本正经地胡说八道”时，第一反应是这AI不行，算法写错了，或者训练数据还不够。事实上，AI幻觉，是当前AI模型工作机制的必然产物，甚至可以说，是其具备“创造力”的源泉。

我们可以先看看人类自己。有一张非常经典的视觉误差图片，即棋盘阴影错觉：在绿色圆柱体投下的阴影中，棋盘格上标出了方块A和方块B。问题是，A和B的背景色哪一个更深一点？

绝大多数人看第一眼，都会笃定地认为，处在亮部的A是深灰色，而处在阴影中的B是浅色。但如果你用电脑上的取色器去提取它们的物理像素，会震惊地发现：A和B是完完全全相同的灰色。

在绿色圆柱体阴影和周围黑白棋盘格的干扰下，我们的大脑骗了我们，“固执”地按照生活经验进行了加工。无论你凑多近看，这种视觉误差依然存在。

人类为什么会产生这种“幻觉”？其实人类的大脑本身就是一台极其高级的“预测机”。处理视觉信息时，大脑并不是像照相机一样死板地记录像素，而是会根据周围光影、上下文环境和历史经验，自动“脑补”并“构建”出最符合逻辑的现实。

在99%的情况下，大脑的这种“脑补”帮助我们快速理解立体世界；但在那1%的特殊图形里，大脑猜错了，于是就形成了视觉幻觉。

AI模型的工作原理，与人类大脑的这种预测机制惊人地相似。其本质是一个“概率黑盒”，AI根据海量数据学习了人类语言的统计规律，核心任务永远只有一个，就是根据上下文，预测下一个最可能出现的词元。

AI“顺水推舟”地生成文本，当遇到的问题在训练数据中有强烈关联时，便能输出令人惊艳的正确答案；而当遇到盲区时，其机制依然会驱使其按照概率去“顺”出一个听起来最合理的句子，这就导致了AI会“自信地”编造信息。

因此，AI产生幻觉，就像人类看错阴影中A和B的颜色一样，是一种自然的、底层的运行机制。

对于这一点，很多顶级AI研究者都有类似看法。OpenAI前联合创始人安德烈·卡尔帕（Andrej Karpathy）就提出过一个非常精彩的观点：我们不应该把大语言模型看作某种绝对严谨的搜索引擎或知识库，而更应该把它看成一台“造梦机”。

在他看来，大模型本质上就是在“做梦”。我们输入提示词，其实是在引导它的梦境走向。所谓“幻觉”，并不是模型在正常运行中偶然出了错，而是它默认的运行状态。

当大模型的“梦境”恰好与现实相吻合时，我们称之为“正确回答”；而当其“梦境”偏离事实依据，只是按照语言概率惯性滑行时，我们就称之为“幻觉”。

也正因为这种基于概率的“脑补”能力，AI才能写出莎士比亚风格的诗歌，才能帮我们构思科幻小说的剧情。如果我们彻底锁死幻觉，要求它必须100%基于已有事实输出，那么AI也会同时丧失创造力、泛化能力和“像人一样的灵性”，退化成一个死板的传统数据库。

02

解决AI幻觉的必要性

既然幻觉是AI的特点，是创造力的源泉，为什么整个行业还要如此紧张地去解决它？

如果AI只是陪人聊天、写写文章、做个表情包，出现幻觉也无大碍。但让AI去做金融量化交易，去辅助自动驾驶，去参与医疗判断，去设计高精度的半导体芯片，容错率几乎为零。

AI幻觉最危险的地方，是会用流畅、完整甚至带着权威感的语言，把错误包装成一种看似成熟的结论。

对于专家来说，错误也许还能被识别；但对于还没有形成专业判断力的使用者，尤其是学生、初入行业的从业者，或者跨领域使用AI的人来说，这种“貌似正确”的答案反而最容易被直接接受。

这就造成一种新的认知风险——过去人们查资料，至少还会看到出处、版本和上下文。现在被AI重新组织过的答案，却不知道其中哪些来自真实资料，哪些只是模型顺着语言概率“编”出来的。

学生可能把错误解释当成知识框架，年轻从业者可能把错误建议带入工作流程，普通用户也可能在法律、健康、金融等高风险问题上做出错误决定。这些都是“AI幻觉”最令人担忧的隐患和危害。

这正是大模型走向高阶应用时绕不开的一道门槛。只会给出答案却无法自证过程的黑盒系统，很难被真正托付。

03

解决AI幻觉的不同路径探索

诚然，这并不意味着行业除了Axiom的形式化验证之外，就完全没有其他路线。只是目前来看，不同路线解决的是不同层级的问题。

第一类是“让AI有据可查”。最典型的是RAG，也就是检索增强生成。让模型回答前先检索企业知识库、论文、法律条文或产品文档，再根据检索结果生成答案。但检索到的资料可能不完整，模型可能误读资料，引用也可能和结论之间并不真正匹配。

因此，RAG更像是给AI接上一套外部记忆，而不是从根本上改变模型的推理机制。

第二类是“让AI学会不乱答”。比如通过训练和评测机制，惩罚模型给出错误答案，奖励其在不确定时说“不知道”、要求更多信息，或者主动给出置信度。

但这种方法提高的是诚实性和校准能力，仍然不能保证每一个结论都被严格证明。

第三类是“让AI互相检查”。例如自我反思、多轮验证、多模型交叉审查、Verifier模型、Critic模型、工具调用检查等。

但这本质上仍然是用一个概率模型去检查另一个概率模型，最多是把错误率降下来。

第四类是“把AI接入外部工具和结构化系统”。例如计算器、数据库、知识图谱、代码解释器、仿真平台、编译器、搜索引擎和规则引擎。把数字计算交给计算器，把代码运行交给编译器等。

这是非常实用的工程路线，也是目前中国很多企业级大模型落地时更常见的方向。

综上可知，面对AI幻觉，以上这些传统做法更像是在“打补丁”，底层的概率黑盒依然存在，治标不治本。至少到目前，还没有一种通用方案，能够在所有开放场景中达到“形式化验证”那种确定性。

04

为什么是形式化验证？

Axiom的思路则完全不同，他们祭出了计算机科学中最冷门但也最硬核的武器——形式化验证，就是要求把每一步推理都写成机器能检查的、严丝合缝的逻辑链条。

这意味着，它并不是简单让AI少说错话，而是试图让AI在关键问题上把“听起来对”变成“可以被验证为对”。

Axiom引入了一种神奇的、可以自验证的数学编程语言——Lean语言。

这套体系构想精妙之处在于，没有试图去剥夺大模型的“直觉”和“创造力”，而是给这个“造梦机”配上了一个铁面无私的“逻辑裁判”。

在Axiom的系统中，AI模型依然负责发挥其长处：负责猜想、负责搜索、负责产生直觉和灵感。而产出的每一步推理，都必须用Lean语言这种形式化的数学语言写出来，交给后台系统去“验算”。

只要中间有一步逻辑跳跃了、糊弄了，Lean语言的验证系统就不给通过，直接打回去让大模型重新推导。只要结论是从前提里一步步合法推导出来的，那答案就具有了绝对的、可证伪的确定性。

值得注意的是，这条路线并不只有硅谷在探索。我国近年也开始把“可验证AI”作为大模型可靠性的重要方向来推进，已有团队围绕自然语言数学问题到形式化证明代码的自动转换展开研究和竞赛实践。

2026年4月初，北京大学AI4Math团队提出了一个由两个智能体组成的框架：一个叫Rethlas，负责像数学家一样用自然语言寻找证明思路；另一个叫Archon，负责把这些思路转化为Lean 4形式化证明代码，并交给机器证明系统逐步检查。

该模式同样兼顾两大核心诉求，既要AI“说得更像正确答案”，也要AI的数学推理必须通过形式化系统的逻辑检验。

不过，该领域仍处于早期阶段。形式化验证的门槛很高，需要数学、逻辑和编程语言理论，以及庞大的形式化知识库。短期内不太可能替代所有AI幻觉治理方法，而更可能先在数学、代码、科研、芯片和安全协议等高价值、高风险领域形成突破。

对于更广泛的日常应用，目前更现实的做法，仍然是把RAG、知识图谱、领域数据、人工审核和工具调用组合起来，把幻觉率降到可控范围内。

幻觉来自大模型的底层机制，也正是这种概率性的生成能力，让AI拥有了联想、迁移和创造的可能。同时，我们也必须看到，当AI从“会说话的工具”变成“能参与决策的系统”时，幻觉就可能成为社会风险、教育风险和工业风险。

Axiom的意义也正在这里，解决AI幻觉，就是让其在关键问题上接受比人类直觉更严格的验证。接受AI的创造力，同时用数学、逻辑、工具和制度去约束它的行为轨迹，这也许才是AI真正走向可信、可用、可托付的必经之路。